Nuprl Lemma : nequal_wf
13,42
postcript
pdf
A
:Type,
x
,
y
:
A
.
x
y
A
latex
Up
core
2
,
core
2
Definitions
a
b
T
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
not
wf
origin
A:Type, x, y:A. x 
y 
A 
A:Type, x, y:A. x y A b T Tx:A. B(x)